$\forall$${\it es}$:event\_system\{i:l\}, $i$:Id.
\\[0ex]es{-}send(${\it es}$; $i$) $\in$ $k$:Knd$\rightarrow$es{-}kindtype(${\it es}$; $i$; $k$)$\rightarrow$es{-}state(${\it es}$; $i$)$\rightarrow$(es{-}Msg(${\it es}$) List)